/**CFile***********************************************************************

  FileName    [ltlCmd.c]

  PackageName [ltl]

  Synopsis    [Shell commands to deal with the LTL model checking.]

  Description [Shell commands to deal with the LTL model checking.]

  SeeAlso     [mc]

  Author      [Marco Roveri]

  Copyright   [
  This file is part of the ``ltl'' package of NuSMV version 2. 
  Copyright (C) 1998-2001 by CMU and ITC-irst. 

  NuSMV version 2 is free software; you can redistribute it and/or 
  modify it under the terms of the GNU Lesser General Public 
  License as published by the Free Software Foundation; either 
  version 2 of the License, or (at your option) any later version.

  NuSMV version 2 is distributed in the hope that it will be useful, 
  but WITHOUT ANY WARRANTY; without even the implied warranty of 
  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU 
  Lesser General Public License for more details.

  You should have received a copy of the GNU Lesser General Public 
  License along with this library; if not, write to the Free Software 
  Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307  USA.

  For more information on NuSMV see <http://nusmv.irst.itc.it>
  or email to <nusmv-users@irst.itc.it>.
  Please report bugs to <nusmv-users@irst.itc.it>.

  To contact the NuSMV development board, email to <nusmv@irst.itc.it>. ]

******************************************************************************/

#if HAVE_CONFIG_H
# include "config.h"
#endif

#include "ltlInt.h" 
#include "prop/prop.h"
#include "cmd/cmd.h"
#include "mc/mc.h"
#include "utils/error.h" /* for CATCH */
#include "enc/enc.h"

static char rcsid[] UTIL_UNUSED = "$Id: ltlCmd.c,v 1.13.2.6.4.5 2006/05/19 08:09:16 nusmv Exp $";

int CommandCheckLtlSpec(int argc, char ** argv);

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/
static int UsageCheckLtlSpec ARGS((void));

/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/

/**Function********************************************************************

  Synopsis           [Initializes the ltl package.]

  Description        [Initializes the ltl package.]

  SideEffects        [None]

******************************************************************************/
void Ltl_Init(void)
{
  Cmd_CommandAdd("check_ltlspec", CommandCheckLtlSpec, 0, false);
}

/**Function********************************************************************

  Synopsis           [Performs LTL model checking]

  CommandName        [check_ltlspec]       

  CommandSynopsis    [Performs LTL model checking]  

  CommandArguments   [\[-h\] \[-m | -o output-file\] \[-n number | -p "ltl-expr \[IN context\]"\] ] 

  CommandDescription [ Performs model checking of LTL formulas. LTL
  model checking is reduced to CTL model checking as described in the
  paper by \[CGH97\].<p>

  A <tt>ltl-expr</tt> to be checked can be specified at command line 
  using option <tt>-p</tt>. Alternatively, option <tt>-n</tt> can be used
  for checking a particular formula in the property database. If 
  neither <tt>-n</tt> nor <tt>-p</tt> are used, all the LTLSPEC formulas in
  the database are checked.<p>

  Command options:<p>
  <dl>
    <dt> <tt>-m</tt>
       <dd> Pipes the output generated by the command in processing
           <tt>LTLSPEC</tt>s to the program specified by the
           <tt>PAGER</tt> shell variable if defined, else
           through the Unix command "more".
    <dt> <tt>-o output-file</tt>
       <dd> Writes the output generated by the command in processing
           <tt>LTLSPEC</tt>s to the file <tt>output-file</tt>.
    <dt> <tt>-p "ltl-expr \[IN context\]"</tt>
       <dd> An LTL formula to be checked. <tt>context</tt> is the module 
       instance name which the variables in <tt>ltl_expr</tt> must be 
       evaluated in.
    <dt> <tt>-n number</tt>
       <dd> Checks the LTL property with index <tt>number</tt> in the property
            database.
  </dl>]

  SideEffects        [None]

******************************************************************************/
int CommandCheckLtlSpec(int argc, char **argv)
{
  int c;
  int prop_no = -1;
  char* formula = NIL(char);
  int status = 0;
  int useMore = 0;
  char* dbgFileName = NIL(char);
  FILE* old_nusmv_stdout = NIL(FILE);

  util_getopt_reset();
  while ((c = util_getopt(argc,argv,"hmo:n:p:")) != EOF) {

    switch (c) {
    case 'h': return UsageCheckLtlSpec();

    case 'n':
      if (formula != NIL(char)) return UsageCheckLtlSpec();
      if (prop_no != -1) return UsageCheckLtlSpec();
      
      prop_no = PropDb_get_prop_index_from_string(util_optarg);
      if (prop_no == -1) return 1;
      break;

    case 'p':
      if (prop_no != -1) return UsageCheckLtlSpec();
      if (formula != NIL(char)) return UsageCheckLtlSpec();
      
      formula = util_strsav(util_optarg);
      break;

    case 'o':
      if (useMore == 1) return UsageCheckLtlSpec();
      dbgFileName = util_strsav(util_optarg);
      fprintf(nusmv_stdout, "Output to file: %s\n", dbgFileName);
      break;

    case 'm':
      if (dbgFileName != NIL(char)) return UsageCheckLtlSpec();
      useMore = 1;
      break;
      
    default:  return UsageCheckLtlSpec();
    }
  }
  if (argc != util_optind) return UsageCheckLtlSpec();

  if (cmp_struct_get_read_model(cmps) == 0) {
    fprintf(nusmv_stderr,
            "A model must be read before. Use the \"read_model\" command.\n");
    return 1;
  }

  if (cmp_struct_get_encode_variables(cmps) == 0) {
    fprintf(nusmv_stderr, 
            "The variables must be built before. Use the \"encode_variables\" command.\n");
    return 1;
  }

  if ( (!cmp_struct_get_build_model(cmps)) 
       && (opt_cone_of_influence(options) == false) ) {
    fprintf(nusmv_stderr, "The current partition method %s has not yet be computed.\n", 
	    TransType_to_string(get_partition_method(options)));
    fprintf(nusmv_stderr, "Use \t \"build_model -f -m %s\"\nto build the transition relation.\n", 
	    TransType_to_string(get_partition_method(options)));
    return 1;
  }

  if (useMore) {
    old_nusmv_stdout = nusmv_stdout;
    nusmv_stdout = CmdOpenPipe(useMore);
    if (nusmv_stdout==(FILE*) NULL) {nusmv_stdout=old_nusmv_stdout; return 1;}
  }

  if (dbgFileName != NIL(char)) {
    old_nusmv_stdout = nusmv_stdout;
    nusmv_stdout = CmdOpenFile(dbgFileName);
    if (nusmv_stdout==(FILE*) NULL) {nusmv_stdout = old_nusmv_stdout; return 1;}
  }
  
  if (formula != NIL(char)) {
    prop_no = PropDb_prop_parse_and_add(Compile_get_global_symb_table(), 
					formula, Prop_Ltl);

    if (prop_no == -1) { status = 1; goto check_ltlspec_exit; /* error */ }

    CATCH {
      PropDb_verify_prop_at_index(prop_no);
    }
    FAIL {
      status = 1;
    }
  }
  else if (prop_no != -1) {
    if (Prop_check_type(PropDb_get_prop_at_index(prop_no), Prop_Ltl) != 0) {
      status = 1;
    }
    else {
      CATCH {
        PropDb_verify_prop_at_index(prop_no);
      }
      FAIL {
        status = 1;
      }
    }
  }
  else {
    CATCH {
      PropDb_verify_all_type(Prop_Ltl);
    }
    FAIL {
      status = 1;
    }
  }

check_ltlspec_exit:   /* clean exit */  
  if (useMore) {
    CmdClosePipe(nusmv_stdout);
    nusmv_stdout = old_nusmv_stdout;
  }

  if (dbgFileName != NIL(char)) {
    CmdCloseFile(nusmv_stdout);
    nusmv_stdout = old_nusmv_stdout;
  }

  return status;
}

static int UsageCheckLtlSpec()
{
  fprintf(nusmv_stderr, "usage: check_ltlspec [-h] [-m | -o file] [-n number | -p \"ltl_expr\"]\n");
  fprintf(nusmv_stderr, "   -h \t\t\tPrints the command usage.\n");
  fprintf(nusmv_stderr, "   -m \t\t\tPipes output through the program specified by\n");
  fprintf(nusmv_stderr, "      \t\t\tthe \"PAGER\" environment variable if any,\n");
  fprintf(nusmv_stderr, "      \t\t\telse through the UNIX command \"more\".\n");
  fprintf(nusmv_stderr, "   -o file\t\tWrites the debugger output to \"file\".\n");
  fprintf(nusmv_stderr, "   -n number\t\tChecks only the LTLSPEC with the given index number.\n");
  fprintf(nusmv_stderr, "   -p \"ltl-expr\"\tChecks only the given LTL formula.\n");
  return(1);
}
